Nuprl Lemma : w-kind-lemma
0,22
postcript
pdf
w
:World,
e
:E. kind(
e
) ~ kind(a(loc(
e
);time(
e
)))
latex
Definitions
tag(
k
)
,
lnk(
k
)
,
act(
k
)
,
islocal(
k
)
,
rcv(
l
,
tg
)
,
locl(
a
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
x
:
A
B
(
x
)
,
left
+
right
,
Knd
,
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
:
A
B
(
x
)
,
s
=
t
,
act(
e
)
,
kind(
e
)
,
kind(
e
)
,
w-info(
w
;
e
)
,
b
,
{
x
:
A
|
B
(
x
) }
,
E
,
World
,
<
a
,
b
>
,
{
T
}
,
SQType(
T
)
,
s
~
t
,
a(
i
;
t
)
,
kind(
a
)
Lemmas
Knd
sq
,
w-E
wf
,
world
wf
,
w-kind
wf
,
w-a
wf
,
Knd
wf
origin
w:World, e:E. kind(e) ~ kind(a(loc(e);time(e))) w:World, e:E. kind(e) ~ kind(a(loc(e);time(e))) 
B(x)
Tx:A. B(x)
Q
B(x)
b